es:ES, l:IdLnk, tg:Id, T:Type.
{m:Msg| source(mlnk(m)) = source(l)  Id }  Msg(l',tg'. if l' = l  tg' = tg T else Top fi)
 (e:E. isrcv(e)  lnk(e) = l  tag(e) = tg  valtype(e)  T) 

latex

Definitions	x:A. B(x), P  Q, if b t else f fi, valtype(e), t  T, true, false, Prop, , Unit, P  Q, P & Q, A, False,
Lemmas	bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, Id wf, es-tag wf, IdLnk wf, es-lnk wf, es-isrcv wf, es-E wf, es-Msg wf, lsrc wf, mlnk wf2, Msg wf, ifthenelse wf, band wf, eq lnk wf, eq id wf, top wf, event system wf